#pragma once
#include "PDTExpBoolBinNum.h"
#include "PDTNumConst.h"
#include "PDTBoolConst.h"

class PDTLessThan :  public PDTExpBoolBinNum, public TraverseIfc <PDTLessThan, PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTLessThan)
public:
	PDTLessThan(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right);
	NodeTypeEnum getType() {
		return PDTLessThan_Em;
	}
	virtual void printType() {
		cout << "PDTLessThan_Em";
	}
	bool isLessThan() {
		return true;
	}

        PDTExpNum * getLeft() {
            return dynamic_cast<PDTExpNum*>(children[0]);
        }

        PDTExpNum * getRight() {
            return dynamic_cast<PDTExpNum*>(children[1]);
        }

	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTNumConstInt* child0 = dynamic_cast<PDTNumConstInt*>(children[0]->getNValue());
		PDTNumConstInt* child1 = dynamic_cast<PDTNumConstInt*>(children[1]->getNValue());
		bool result = child0->getValue() < child1->getValue();
		nValue = new PDTBoolConst(CG, result);
		cout<<"Less than Result: [("<<child0->getValue()<<") < ("<<child1->getValue()<<")] = "<<result<<endl;
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpNum* childZeroClone = (PDTExpNum*)(children[0]->clone(CG));
		PDTExpNum* childOneClone = (PDTExpNum*)(children[1]->clone(CG));
		toReturn = new PDTLessThan(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}

	virtual stringstream & toString(stringstream & ss) const {
		ss << "( ";
		children[0]->toString(ss) << " < ";
		children[1]->toString(ss) << " )";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};

class PDTGreaterThan :  public PDTExpBoolBinNum, public TraverseIfc <PDTGreaterThan, PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTGreaterThan)
public:
	PDTGreaterThan(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right);
	NodeTypeEnum getType() {
		return PDTGreaterThan_Em;
	}
	bool isGreaterThan() {
		return true;
	}

        PDTExpNum * getLeft() {
            return dynamic_cast<PDTExpNum*>(children[0]);
        }

        PDTExpNum * getRight() {
            return dynamic_cast<PDTExpNum*>(children[1]);
        }

	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTNumConstInt* child0 = dynamic_cast<PDTNumConstInt*>(children[0]->getNValue());
		PDTNumConstInt* child1 = dynamic_cast<PDTNumConstInt*>(children[1]->getNValue());
		bool result = child0->getValue() > child1->getValue();
		nValue = new PDTBoolConst(CG, result);
		cout<<"Greater than Result: [("<<child0->getValue()<<") > ("<<child1->getValue()<<")] = "<<result<<endl;
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpNum* childZeroClone = (PDTExpNum*)(children[0]->clone(CG));
		PDTExpNum* childOneClone = (PDTExpNum*)(children[1]->clone(CG));
		toReturn = new PDTGreaterThan(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}

	virtual stringstream & toString(stringstream & ss) const {
		ss << "( ";
		children[0]->toString(ss) << " > ";
		children[1]->toString(ss) << " )";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};

class PDTLessThanEqual :  public PDTExpBoolBinNum, public TraverseIfc <PDTLessThanEqual, PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTLessThanEqual)
public:
	PDTLessThanEqual(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right);
	NodeTypeEnum getType() {
		return PDTLessThanEqual_Em;
	}
	virtual void printType() {
		cout << "PDTLessThanEqual_Em";
	}
	bool isLessThanEqual() {
		return true;
	}
    
	PDTExpNum * getLeft() {
	    return dynamic_cast<PDTExpNum*>(children[0]);
	}

	PDTExpNum * getRight() {
	    return dynamic_cast<PDTExpNum*>(children[1]);
	}

	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTNumConstInt* child0 = dynamic_cast<PDTNumConstInt*>(children[0]->getNValue());
		PDTNumConstInt* child1 = dynamic_cast<PDTNumConstInt*>(children[1]->getNValue());
		bool result = child0->getValue() <= child1->getValue();
		nValue = new PDTBoolConst(CG, result);
		cout<<"Less than or equal Result: [("<<child0->getValue()<<") <= ("<<child1->getValue()<<")] = "<<result<<endl;
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpNum* childZeroClone = (PDTExpNum*)(children[0]->clone(CG));
		PDTExpNum* childOneClone = (PDTExpNum*)(children[1]->clone(CG));
		toReturn = new PDTLessThanEqual(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}

	virtual stringstream & toString(stringstream & ss) const {
		ss << "( ";
		children[0]->toString(ss) << " <= ";
		children[1]->toString(ss) << " )";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};

class PDTGreaterThanEqual :  public PDTExpBoolBinNum, public TraverseIfc <PDTGreaterThanEqual, PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTGreaterThanEqual)
public:
	PDTGreaterThanEqual(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right);
	NodeTypeEnum getType() {
		return PDTGreaterThanEqual_Em;
	}

	bool isGreaterThanEqual() {
		return true;
	}

	PDTExpNum * getLeft() {
	    return dynamic_cast<PDTExpNum*>(children[0]);
	}

	PDTExpNum * getRight() {
	    return dynamic_cast<PDTExpNum*>(children[1]);
	}
	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTNumConstInt* child0 = dynamic_cast<PDTNumConstInt*>(children[0]->getNValue());
		PDTNumConstInt* child1 = dynamic_cast<PDTNumConstInt*>(children[1]->getNValue());
		bool result = child0->getValue() >= child1->getValue();
		nValue = new PDTBoolConst(CG, result);
		cout<<"Greater than or equal Result: [("<<child0->getValue()<<") >= ("<<child1->getValue()<<")] = "<<result<<endl;
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpNum* childZeroClone = (PDTExpNum*)(children[0]->clone(CG));
		PDTExpNum* childOneClone = (PDTExpNum*)(children[1]->clone(CG));
		toReturn = new PDTGreaterThanEqual(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}

	virtual stringstream & toString(stringstream & ss) const {
		ss << "( ";
		children[0]->toString(ss) << " >= ";
		children[1]->toString(ss) << " )";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};

class PDTEqualNum :  public PDTExpBoolBinNum, public TraverseIfc <PDTEqualNum, PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTEqualNum)
public:
	PDTEqualNum(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right);

	NodeTypeEnum getType() {
		return PDTEqualNum_Em;
	}
	bool isEqualNum() {
		return true;
	}

    PDTExpNum *  getLeft() {
        return dynamic_cast<PDTExpNum*>(children[0]);
    }

    PDTExpNum * getRight() {
        return dynamic_cast<PDTExpNum*>(children[1]);
    }

	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTNumConstInt* child0 = dynamic_cast<PDTNumConstInt*>(children[0]->getNValue());
		PDTNumConstInt* child1 = dynamic_cast<PDTNumConstInt*>(children[1]->getNValue());
		bool result = (child0->getValue() == child1->getValue());
		nValue = new PDTBoolConst(CG, result);
		cout<<"Num equal Result: [("<<child0->getValue()<<") == ("<<child1->getValue()<<")] = "<<result<<endl;
		return true;
	}


	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpNum* childZeroClone = (PDTExpNum*)(children[0]->clone(CG));
		PDTExpNum* childOneClone = (PDTExpNum*)(children[1]->clone(CG));
		toReturn = new PDTEqualNum(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}

	virtual stringstream & toString(stringstream & ss) const {
		ss << "( ";
		children[0]->toString(ss) << " = ";
		children[1]->toString(ss) << " )";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};

class PDTNotEqualNum :  public PDTExpBoolBinNum, public TraverseIfc <PDTNotEqualNum, PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTNotEqualNum)
public:
	PDTNotEqualNum(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right);

	NodeTypeEnum getType() {
		return PDTNotEqualNum_Em;
	}
	bool isNotEqualNum() {
		return true;
	}

    PDTExpNum *  getLeft() {
        return dynamic_cast<PDTExpNum*>(children[0]);
    }

    PDTExpNum * getRight() {
        return dynamic_cast<PDTExpNum*>(children[1]);
    }

	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTNumConstInt* child0 = dynamic_cast<PDTNumConstInt*>(children[0]->getNValue());
		PDTNumConstInt* child1 = dynamic_cast<PDTNumConstInt*>(children[1]->getNValue());
		bool result = child0->getValue() != child1->getValue();
		nValue = new PDTBoolConst(CG, result);
		cout<<"Num not equal Result: [("<<child0->getValue()<<") != ("<<child1->getValue()<<")] = "<<result<<endl;
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpNum* childZeroClone = (PDTExpNum*)(children[0]->clone(CG));
		PDTExpNum* childOneClone = (PDTExpNum*)(children[1]->clone(CG));
		toReturn = new PDTNotEqualNum(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}

	virtual stringstream & toString(stringstream & ss) const {
		ss << "( ";
		children[0]->toString(ss) << " != ";
		children[1]->toString(ss) << " )";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};
